$\forall$$M$:MsgA. Trans($M$) $\in$ $k$:Knd$\rightarrow$$M$.da($k$)$\rightarrow$$M$.state$\rightarrow$$M$.state